This is TeX, WAITS Version 1.3 (preloaded format=plain 85.1.8)  25 JAN 1985 11:34
**CIRNEW.TEX
(CIRNEW.TEX[S79,JMC] (JMCMAC.TEX[1,SMC]
\hours=\count25
\minutes=\count26
\temp=\count27
\ampm=\toks12
\scount=\count28
\ecount=\count29
\itemcount=\count30
\subcount=\count31
\notecount=\count32
\partcount=\count33
\outlcount=\count34
\supcount=\count35
\parcount=\count36
) [1] [2] [3] [4] [5]
Overfull \hbox (3.78075pt too wide) in paragraph at lines 3--8, p.6
[]\tenrm Let $\tenit A$ \tenrm be a sen-tence of first or-der logic con-tain-ing
 a pred-i-cate sym-bol $\tenit P\tenrm (\tenit x[]\teni ; [] [] ; \tenit x[]$

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\hbox(0.0+0.0)x20.0
.\tenrm L
.\tenrm e
.\tenrm t
.\glue 3.33333 plus 1.66666 minus 1.1111
.etc.

[6] [7]
Overfull \hbox (5.97314pt too wide) detected at line 115, p.6
\tenit λ [] \tenrm (\tenit 0\tenrm ) [] \tensy ↑ [] 8\tenit x\teni :\tenrm (\ten
it λ [] \tenrm (\tenit x\tenrm ) [] \tensy ↑↑[ [] \tenit λ [] \tenrm (\tenit suc
c [] x\tenrm )) [] \tensy ↑ [] 8\tenit x\teni :\tenrm (\tenit λ [] \tenrm (\teni
t x\tenrm ) [] \tensy ↑↑[ [] \tenit isnatnum [] x\tenrm ) [] \tensy ↑↑[ [] [] 8\
tenit x\teni :\tenrm (\tenit isnatnum [] x [] \tensy ↑↑[ [] \tenit λ [] \tenrm (
\tenit x\tenrm ))\teni :

\hbox(7.5+2.5)x361.34999, glue set - 1.0
.\tenit λ
.\kern0.5986
.\glue(\thinmuskip) 1.66663
.\hbox(0.0+0.0)x-1.66663
..\kern-1.66663
.\glue(\thinmuskip) 1.66663
.etc.

[8] [9] [10] [11] [12] [13] [14] [15]
Output written on CIRNEW.DVI[S79,JMC] (15 pages, 48216 bytes).